i, a, x:Id, X, T:Type, x0:X, P:(XTProp), es:ES. pre-init1-p(es;i;x;X;x0;a;T;P)  Prop 

latex

Definitions	t  T, x:A. B(x), @i x initially v:T, Type, vartype(i;x), P  Q, b, Void, x:AB(x), False, A, x:AB(x), Id, ES, locl(a), A/x,y. B(x;y), 1of(t), E, s = t, left+right, P  Q, e  e' , (x after e), Prop, f(a), Knd, kind(e), A & B, x:A. B(x), loc(e), val(e), x when e, valtype(e), P & Q, e@i. P(e), ee'.P(e'), pre-init1-p(es;i;x;X;x0;a;T;P)
Lemmas	event system wf, es-valtype wf, es-when wf, es-val wf, Id wf, es-loc wf, es-E wf, es-le wf, Knd wf, es-kind wf, locl wf, not wf, subtype rel self, es-after wf, es-le-loc, es-loc-pred, es-vartype wf, init-p wf